$\forall$$A$:Type, ${\it as}$:($A$ List). ($\neg$(${\it as}$ = [])) $\Leftarrow\!\Rightarrow$ ($\parallel$${\it as}$$\parallel$ $\geq$ 1 )